\begin{tabbing}
es{-}ble\=\{i:l\}\+
\\[0ex](${\it es}$; $e$; ${\it e'}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case TERMOF\{decidable\_\_es{-}le:ObjectId, 1:l, i:l\}(${\it es}$,${\it e'}$,$e$)\+
\\[0ex]o\=f inl($x$) =$>$ tt\+
\\[0ex]$\mid$ inr($x$) =$>$ ff
\-\-
\end{tabbing}